Termination Proofs for Ground Rewrite Systems – Interpretations and Derivational Complexity
Identifieur interne : 009270 ( Main/Exploration ); précédent : 009269; suivant : 009271Termination Proofs for Ground Rewrite Systems – Interpretations and Derivational Complexity
Auteurs : Dieter Hofbauer [États-Unis]Source :
- Applicable Algebra in Engineering, Communication and Computing [ 0938-1279 ] ; 2001-06-01.
English descriptors
- KwdEn :
Abstract
Abstract.: It is shown that finite terminating ground term rewrite systems have linearly bounded derivational complexity. This is proven via some suitable interpretation into the natural numbers. Terminating ground systems are not necessarily totally terminating, i.e., a strictly monotone interpretation into a well-order might not exist. We show, however, that those systems are almostω-terminating in the sense that such an interpretation into the sum of a finite partial order and the natural numbers always effectively exists. Finally, we show that for ground systems total termination is equivalent to ω-termination, and that this is a decidable property.
Url:
DOI: 10.1007/s002000100062
Affiliations:
Links toward previous steps (curation, corpus...)
- to stream Istex, to step Corpus: 003C35
- to stream Istex, to step Curation: 003B91
- to stream Istex, to step Checkpoint: 001E12
- to stream Main, to step Merge: 009792
- to stream Main, to step Curation: 009270
Le document en format XML
<record><TEI wicri:istexFullTextTei="biblStruct"><teiHeader><fileDesc><titleStmt><title xml:lang="en">Termination Proofs for Ground Rewrite Systems – Interpretations and Derivational Complexity</title><author><name sortKey="Hofbauer, Dieter" sort="Hofbauer, Dieter" uniqKey="Hofbauer D" first="Dieter" last="Hofbauer">Dieter Hofbauer</name></author></titleStmt><publicationStmt><idno type="wicri:source">ISTEX</idno><idno type="RBID">ISTEX:FB8EF420B4D73E3500094FD3BB1315BE364A2B8C</idno><date when="2001" year="2001">2001</date><idno type="doi">10.1007/s002000100062</idno><idno type="url">https://api.istex.fr/ark:/67375/VQC-0S2T044N-8/fulltext.pdf</idno><idno type="wicri:Area/Istex/Corpus">003C35</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Corpus" wicri:corpus="ISTEX">003C35</idno><idno type="wicri:Area/Istex/Curation">003B91</idno><idno type="wicri:Area/Istex/Checkpoint">001E12</idno><idno type="wicri:explorRef" wicri:stream="Istex" wicri:step="Checkpoint">001E12</idno><idno type="wicri:doubleKey">0938-1279:2001:Hofbauer D:termination:proofs:for</idno><idno type="wicri:Area/Main/Merge">009792</idno><idno type="wicri:Area/Main/Curation">009270</idno><idno type="wicri:Area/Main/Exploration">009270</idno></publicationStmt><sourceDesc><biblStruct><analytic><title level="a" type="main" xml:lang="en">Termination Proofs for Ground Rewrite Systems – Interpretations and Derivational Complexity</title><author><name sortKey="Hofbauer, Dieter" sort="Hofbauer, Dieter" uniqKey="Hofbauer D" first="Dieter" last="Hofbauer">Dieter Hofbauer</name><affiliation wicri:level="2"><country xml:lang="fr">États-Unis</country><placeName><region type="state">Delaware</region></placeName><wicri:cityArea>Universität GH Kassel, Fachbereich 17 Mathematik/Informatik, 34109 Kassel, Germany (e-mail: dieter@theory.informatik.uni-kassel.de)</wicri:cityArea></affiliation></author></analytic><monogr></monogr><series><title level="j">Applicable Algebra in Engineering, Communication and Computing</title><title level="j" type="abbrev">AAECC</title><idno type="ISSN">0938-1279</idno><idno type="eISSN">1432-0622</idno><imprint><publisher>Springer-Verlag</publisher><pubPlace>Berlin Heidelberg</pubPlace><date type="published" when="2001-06-01">2001-06-01</date><biblScope unit="volume">12</biblScope><biblScope unit="issue">1-2</biblScope><biblScope unit="page" from="21">21</biblScope><biblScope unit="page" to="38">38</biblScope></imprint><idno type="ISSN">0938-1279</idno></series></biblStruct></sourceDesc><seriesStmt><idno type="ISSN">0938-1279</idno></seriesStmt></fileDesc><profileDesc><textClass><keywords scheme="KwdEn" xml:lang="en"><term>Keywords: Term rewriting systems, Ground rewriting, Termination proofs, Derivational complexity.</term></keywords></textClass><langUsage><language ident="en">en</language></langUsage></profileDesc></teiHeader><front><div type="abstract" xml:lang="en">Abstract.: It is shown that finite terminating ground term rewrite systems have linearly bounded derivational complexity. This is proven via some suitable interpretation into the natural numbers. Terminating ground systems are not necessarily totally terminating, i.e., a strictly monotone interpretation into a well-order might not exist. We show, however, that those systems are almostω-terminating in the sense that such an interpretation into the sum of a finite partial order and the natural numbers always effectively exists. Finally, we show that for ground systems total termination is equivalent to ω-termination, and that this is a decidable property.</div></front></TEI><affiliations><list><country><li>États-Unis</li></country><region><li>Delaware</li></region></list><tree><country name="États-Unis"><region name="Delaware"><name sortKey="Hofbauer, Dieter" sort="Hofbauer, Dieter" uniqKey="Hofbauer D" first="Dieter" last="Hofbauer">Dieter Hofbauer</name></region></country></tree></affiliations></record>Pour manipuler ce document sous Unix (Dilib)
EXPLOR_STEP=$WICRI_ROOT/Wicri/Lorraine/explor/InforLorV4/Data/Main/Exploration
HfdSelect -h $EXPLOR_STEP/biblio.hfd -nk 009270 | SxmlIndent | more
Ou
HfdSelect -h $EXPLOR_AREA/Data/Main/Exploration/biblio.hfd -nk 009270 | SxmlIndent | more
Pour mettre un lien sur cette page dans le réseau Wicri
{{Explor lien
|wiki= Wicri/Lorraine
|area= InforLorV4
|flux= Main
|étape= Exploration
|type= RBID
|clé= ISTEX:FB8EF420B4D73E3500094FD3BB1315BE364A2B8C
|texte= Termination Proofs for Ground Rewrite Systems – Interpretations and Derivational Complexity
}}
| This area was generated with Dilib version V0.6.33. |  |